Functional equivalence checking is an important aspect of electronic design automation (EDA). Functional equivalence checking is routinely used during integrated circuit design to ensure that two different representations of a circuit design exhibit the same behavior. As the circuit design moves through different phases of the design cycle and/or different optimizations are applied to the circuit design, functional equivalence checking may be performed to ensure that the optimizations introduced into the circuit design do not change behavior of the circuit design. This may include ensuring that the latency of the circuit design has not become unbalanced.
In the context of sequential logic synthesis, for example, where retiming and/or pipelining operations may be performed on the circuit design, the complexity of verifying equivalence of circuit design latency is further exacerbated due, at least in part, to changes in flip-flop positions within the circuit design. In the case of retiming, for example, formal verification is typically performed. In the usual case, users define elaborate flip-flop mapping rules and provide the rules to the verification tool. The rules are used to guide the verification tool. The creation of these rules is itself a complex undertaking due, at least in part, to possible cascades of deleted and/or inserted flip-flops. In the case of pipelining, functional equivalence checking is typically performed by simulating the circuit design. The simulation a time-consuming endeavor particularly given the size and complexity of modern circuit designs.